/*
 * 
 */
package milecToMinisat;

import java.io.File ;
import java.io.IOException;

/** 
 * This interface describes the API of milecToMinisat.
 * 
 * @author ter-topcased-ups
 * @version 0.01, 2008/12/03
 * 
 */
public interface ClauseGenerator {
		
	/**
	 * create the integer variable named name with maximum value 
	 * @param name of the new variable
	 * @param maximum value of this variable
	 */
	public IntegerVariable declareInteger(String name, int maximum ) ;
	
	/**
	 * add a constraint to the model to be checked
	 * @param exp an {@link IntegerExp}
	 * @param constraintType
	 * @param cst, an IntegerCst (constructed with new IntegerCst(int n) )
	 */
	public void addIntegerConstraint(IntegerExp exp,
			IntegerConstraintType constraintType ,IntegerCst cst) ;
	
	/**
	 * check satisfiability of the previous defined model ;
	 */
	public boolean checkModel() ;
	
	/**
	 * write in aFile the minisat clauses.
	 * @param aFile where write clauses. 
	 */
	public void  writeIn(File aFile) throws IOException ;
}
